
(set-info :smt-lib-version 2.6)
(set-logic QF_FFA)
(define-sort FF0 () (_ FiniteField 3))
(declare-fun x0 () FF0)
(declare-fun x1 () FF0)
(declare-fun x2 () FF0)
(declare-fun x3 () FF0)
(declare-fun x4 () FF0)
(declare-fun x5 () FF0)
(declare-fun x6 () FF0)
(declare-fun x7 () FF0)
(assert
  (let ((let0 (ff.mul (as ff2 FF0) x1 x4 x7)))
  (let ((let1 (ff.mul x4 x7)))
  (let ((let2 (ff.add let0 let1)))
  (let ((let3 (= let2 (as ff0 FF0))))
  (let ((let4 (ff.mul x1 x1 x6)))
  (let ((let5 (ff.mul (as ff2 FF0) x0 x6 x7)))
  (let ((let6 (ff.mul (as ff2 FF0) x2 x7)))
  (let ((let7 (ff.mul (as ff2 FF0) x0)))
  (let ((let8 (ff.add let4 let5 let6 let7)))
  (let ((let9 (= let8 (as ff0 FF0))))
  (let ((let10 (ff.mul x1 x2 x3)))
  (let ((let11 (ff.mul (as ff2 FF0) x2 x2 x4)))
  (let ((let12 (ff.mul (as ff2 FF0) x3 x6 x6)))
  (let ((let13 (ff.mul x6 x6 x6)))
  (let ((let14 (as ff1 FF0)))
  (let ((let15 (ff.add let10 let11 let12 let13 let14)))
  (let ((let16 (= let15 (as ff0 FF0))))
  (let ((let17 (ff.mul (as ff2 FF0) x0 x0)))
  (let ((let18 (ff.mul x3 x6)))
  (let ((let19 (ff.mul (as ff2 FF0) x7)))
  (let ((let20 (ff.add let17 let18 let19)))
  (let ((let21 (= let20 (as ff0 FF0))))
  (let ((let22 (ff.mul (as ff2 FF0) x2 x4 x4)))
  (let ((let23 (ff.mul x2 x3 x6)))
  (let ((let24 (ff.add let22 let23)))
  (let ((let25 (= let24 (as ff0 FF0))))
  (let ((let26 (ff.mul (as ff2 FF0) x0 x3 x3)))
  (let ((let27 (ff.mul (as ff2 FF0) x2 x5 x6)))
  (let ((let28 (ff.mul (as ff2 FF0) x0 x4 x7)))
  (let ((let29 (as ff1 FF0)))
  (let ((let30 (ff.add let26 let27 let28 let29)))
  (let ((let31 (= let30 (as ff0 FF0))))
  (let ((let32 (ff.mul x1 x3 x6)))
  (let ((let33 (ff.mul x2 x6 x6)))
  (let ((let34 (ff.mul x0 x3 x7)))
  (let ((let35 (ff.add let32 let33 let34)))
  (let ((let36 (= let35 (as ff0 FF0))))
  (let ((let37 (ff.mul (as ff2 FF0) x0 x3 x5)))
  (let ((let38 (ff.mul x3 x5 x7)))
  (let ((let39 (ff.mul x1 x6 x7)))
  (let ((let40 (ff.mul (as ff2 FF0) x0 x7)))
  (let ((let41 (ff.add let37 let38 let39 let40)))
  (let ((let42 (= let41 (as ff0 FF0))))
  (let ((let43 (and let3 let9 let16 let21 let25 let31 let36 let42)))
  let43
))))))))))))))))))))))))))))))))))))))))))))
)
(check-sat)
